\section{Running Example (Naive Version)}
\label{sec:Running}

\begin{figure}[t]%
	\includegraphics[width=\columnwidth]{images/NaiveFS-MM.png}%
	\vspace{-0.3cm}
	\caption{Simplified \textsc{Mls} metamodel \cite{Bell:Lapadula:73}, as a Kermeta Class Diagram \cite{Kermeta-Weaving2005}.}%
	\label{fig:MLS-MM}%
		\vspace{-0.5cm}
\end{figure}

Our example is inspired from \cite{ASSE:Cristia}: it is an \textsc{Unix}-like operating system that includes a Multi-Level Security (\textsc{Mls}) File System (\textsc{Fs}). We first present the expected requirements on the file system, then explain its implementation in terms of \textsc{Apn}, and finish with the requirements formalisation in terms of three properties expressed over the \textsc{Apn}. \Sect \ref{sec:Evolving} will then present two manual evolution that iteratively enforce more properties on the system.

\subsection{Requirements}
\label{sec:Running-Requirements}


In \textsc{Mls} \cite{Bell:Lapadula:73}, two concepts are essentially relevant: \emph{objects} designate system resources or data repositories that must be protected (\eg files, directories or terminals); \emph{subjects} denote entities capable of requesting services from system resources (\eg users, or processors). Both are associated to an \emph{access class}: they classify objects and subjects according to their confidentiality, and responsability degree, respectively. Intuitively, an object associated with a high access class can only be seen or manipulated by a highly trusted subject.

For simplification and space limitation purposes, we present a simplified version of a file system consisting only of \emph{files} as possible objects, and \emph{users} as possible subjects. Files can either be read or written by an user, or idle (which implies no simultaneous readings by different users). 

An important quality of such file systems is \emph{confidentiality}, especially against Trojan horses \cite{Abrams:Jajodia:Podell:95}: they consist in code executed by a trusted user without knowing it or consenting for it; they can also pass confidential data by copying sensitive data into files accessible to untrusted users. One common technique for preventing this attack is \emph{data confinement}: a trusted user cannot open simultaneously two files with the most confidential one in read mode and the less confidential in write mode, thus preventing data leaks by copy from the former to the latter.

Therefore in our running example, we aim at enforcing the two following requirements: (\textbf{\texttt{R1}}) a file can be open, either in read or in write mode, only by an user with sufficient access rights; (\textbf{\texttt{R2}}) an user always respects the data confinement condition. 


\subsection{Model-Checking Algebraic Petri Nets with \Alpina}
\label{sec:Alpina}

\Alpina (Algebraic Petri Net Analyzer) is a model-checker developed by the \textsc{Smv} team in Geneva \cite{J:Hostettler-etAl:2011}. \Alpina takes two inputs: an \textsc{APn}, \ie a Petri Net (\textsc{Pn}) whose tokens are terms of an equational algebraic specification (\ie sorts, associated operations and equations), and whose behaviour is graphically defined; and a set of first-order formul\ae\xspace over the specification terms expressing invariants over the \textsc{Pn}. It allows the verification of such formul\ae\xspace by exhaustively exploring the \textsc{Pn} state space. If they are not satisfied, \Alpina returns a possible marking that violates the formul\ae.

In our context, \Alpina is used at each iteration step to check that new properties are satisfied. In case of a revision, the model-checker is run on each previously satisfied properties to ensure they are still satisfied by the revised model. 

%In \Alpina, \textsc{Pn}'s transitions can manipulate variable tokens graphically represented as transitions labels: \eg two transitions in \Fig \ref{fig:naivefs} are labeled with $\mathtt{[\$f]}$: it means each transition can consume a token of $\mathtt{\$f}$'s sort (here, the sort is $\mathtt{File}$, not visible in the \textsc{Pn}).

\subsection{The Naive File System  \emph{$\mathtt{FS}$}}
\label{sec:Running-Naive}

\begin{figure}[t]%
	\begin{minipage}{\columnwidth}
		\begin{minipage}{0.41\columnwidth}
			\begin{footnotesize}
				\begin{tabular}{@{}c | @{}c@{} | c |@{}c@{}}
 					& Name & $\mathtt{SL}$ & $\mathtt{CR}$\\\hline\hline
					\multirow{3}{*}{\rotatebox{90}{Files}}
 					& $\mathtt{f1}$     &     2       & $\mathtt{NATO}$\\
 					& $\mathtt{f2}$     &     0       & $\mathtt{CIA}$\\
 					& $\mathtt{f3}$     &     1       & $\emptyset$\\\hline
					\multirow{3}{*}{\rotatebox{90}{Users}}
 					& $\mathtt{levi}$   &     3       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
 					& $\mathtt{\,eugene\,}$ &     0       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
				\end{tabular}
			\end{footnotesize}
		\end{minipage}%
		\hfill
		\begin{minipage}{0.50\columnwidth}
			\begin{tiny}
				\begin{ttfamily}
					\begin{tabular}{@{}r@{}l}
						M$_{_0}$(files)=& [file(f1, ac(s(s(ZERO)),\\
								   &	\phantom{M} list(NATO, empty)));\\
								   & file(f2, ac(ZERO,\\
								   & \phantom{M} list(CIA, empty)));\\
								   & file(f3, ac(s(ZERO),\\
								   & \phantom{M} empty))]\\
					 	M$_{_0}$(users)=& [user(levi, ac(s(s(s(ZERO))),\\
					 				& 	\phantom{M} list(NATO, list(CIA, empty)))));\\
					 				&  user(eugene, ac(ZERO,\\
					 				& 	\phantom{M} list(NATO, list(CIA, empty)))))]
					\end{tabular}				
				\end{ttfamily}
			\end{tiny}
		\end{minipage}
	\end{minipage}
	\caption{A simple \textsc{Fs} model and the corresponding initial marking.}%
	\label{fig:MLS-M}%
	
	\vspace{-0.4cm}
\end{figure}



Figure \ref{fig:MLS-MM} presents a simplified metamodel for \textsc{Mls} File Systems: it contains only files as objects and only users as subjects. A \textsf{File} and an \textsf{User} consists in a \textsf{name} and an associated \textsf{AccessClass}. An \textsf{AccessClass} is composed of an integer representing a \textsf{securityLevel} and a \textsf{Category} set. A \textsf{Category} is one of the following credential: \textsf{CIA}, \textsf{NATO} or \textsf{NUCLEAR} (represented as an enumeration). Access classes can be compared using the \textsf{dominates} operation: if $\mathsf{ac} = (\mathsf{s}, \mathsf{C})$ and $\mathsf{ac'} = (\mathsf{s'}, \mathsf{C'})$ are two access classes, where $\mathsf{s}, \mathsf{s'}\in \mathbb{N}$ represent security levels and $\mathsf{C}, \mathsf{C'}$ represent sets of credential categories, then $\mathsf{ac}$ \emph{dominates} $\mathsf{ac'}$ (noted $\mathsf{ac} \rhd \mathsf{ac'}$) iff  $\mathsf{ac}$ is ``\emph{stronger}'' than $\mathsf{ac'}$, \ie formally, if $\mathsf{s'}\leq \mathsf{s}$ and $\mathsf{C'} \subseteq \mathsf{C}$). 
Note that this notion of access class domination is different from the one classical in \textsc{Pn}, which operates on markings.

Consider now an \textsc{Mls} \textsc{Fs} model corresponding to the naive \textsc{Fs}, as described in \Fig \ref{fig:MLS-M}: it consists in three files and two users ($\mathtt{SL}$ stands for security level and $\mathtt{CR}$ for credential). Here, the user $\mathtt{levi}$ dominates all files whereas $\mathtt{eugene}$ only dominates file $\mathtt{f2}$. 



For now, any \textsc{Mls Fs} model (like the one depicted in \Fig \ref{fig:MLS-M}, left) conforming to the metamodel of \Fig \ref{fig:MLS-MM} is translated by hand in two steps into an \textsc{Apn}. In the first step, data structures for \textsc{Mls} models are translated into abstract data types: $\mathtt{string}$s used for files and users names become sorts (because we only need to compare them for equality); and security levels are implemented using a Peano-like representation, with $\mathtt{ZERO}$ for $0$ and $\mathtt{s}$ for the successor operation (because we only need an order for comparing them). Following \Alpina's syntax, where variable tokens are prefixed with $\mathtt{\$}$, let $\mathtt{\$f} = (\mathtt{\$fn}, \mathtt{\$ac_{f}})$ and $\mathtt{\$u} = (\mathtt{\$un}, \mathtt{\$ac_{u}})$ be file and user variables of sorts $\mathtt{File}$ and $\mathtt{User}$ respectively, where $\mathtt{\$fn}$ and $\mathtt{\$un}$ are file- and user-names, and $\mathtt{\$ac_{f}}$ and $\mathtt{\$ac_{u}}$ their respective access classes. Two functions are defined on these sorts: $\mathtt{name}$ and $\mathtt{class}$ return respectively the name and the class of a $\mathtt{File}$ or an $\mathtt{User}$.

\begin{figure}[t]
	\centering
	\epsfig{file=images/naive_fs, width=\linewidth}
	\caption{The naive File System $\FS$ with its initial marking $\mathtt{M}$.}
	\label{fig:naivefs}
	
	\vspace{-0.6cm}
\end{figure}


In the second step, we define the naive translational semantics of \textsc{Mls} systems \ie opening/closing files without credential checkings. The resulting \textsc{Apn} contains four places and four transitions. Places $\mathtt{files}$ and $\mathtt{users}$ contain files and users tokens, representing respectively the files and users objects corresponding to the initial marking of \Fig \ref{fig:MLS-M}. When an user wants to read or write a file, the corresponding transition ($\mathtt{openR}$ or $\mathtt{openW}$, respectively) is fired and consumes tokens $\mathtt{\$f}$ from place \textsf{files} and $\mathtt{\$u}$ from place $\mathtt{users}$; then produces a pair $\mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u})$ stored in the corresponding place (either $\mathsf{reading}$ or $\mathsf{writing}$). When $\mathtt{\$u}$ closes $\mathtt{\$f}$, the corresponding $\mathtt{close}$ transition is fired, which checks that $\mathtt{\$f}$ was actually opened by the user that opened it, and produces back tokens $\mathtt{\$f}$ and $\mathtt{\$u}$ into their respective places. Consuming file tokens every time a file is opened prevents another user from opening the same file.

Figure \ref{fig:naivefs} depicts the \textsc{Pn} that corresponds to the naive \textsc{Fs}. The marking of places $\mathtt{reading}$ and $\mathtt{writing}$ is empty (and denoted by empty brackets \texttt{[]}, and the marking for the two other places follows the initial marking of \Fig \ref{fig:MLS-M} (right). The full specifications of abstract data types can be found in \cite{lucio:10}.


%Let us start with the first model which we will call \emph{naive filesystem}.
%The APN model is depicted in \Fig\ref{fig:naivefs} and represents the
%semantics of the operation of a filesystem. The Petri net uses several kinds of
%algebraic tokens\footnote{For the presentation of the \emph{confidential
%filesystem} example we use in this paper names of sorts and operations which,
%despite being self descriptive, for space reasons cannot be formally introduced. 
%
%
%A full description of the algebraic specifications used in the
%\emph{confidential filesystem} example can be found in~\cite{lucio:10}.}: pairs
%belonging to the set $fileName\times accessClass$ are used in place
%\emph{filesystem} to represent file names and their respective access classes;
%pairs belonging to the set $userName\times accessClass$ are used in place
%\emph{users} to represent a sample of users of the filesystem; finally places
%\emph{readFiles} and \emph{writeFiles} hold tokens which are pairs
%$(fileName\times accessClass)\times (userName\times accessClass)$ in order to
%keep track of which file was opened by which user. We do not explicitly define
%the names of the variables that act as weights on the arcs given their type can
%be inferred from the either the origin or the target place of the arc.
%
%The semantics of the \emph{naive filesystem} model in \Fig\ref{fig:naivefs}
%is such that it simulates opening files in read or write mode and closing them
%by firing the \emph{openForRead}, \emph{openForWrite} and \emph{close}
%transitions respectively. The variables on the entry arcs of the transitions
%declare the consumed tokens from the input places and the variables on the
%output arcs of the transitions declare the produced tokens on the output places. Note that, despite the fact that transitions in APN models may be guarded, in this naive version of the confidential filesystem the \emph{openForRead} and \emph{openForWrite} transitions we do not check if the the user has permission to access a given file.
%

\subsection{Requirements Properties}
\label{sec:Running-Properties}


The requirements of \Sect \ref{sec:Running-Requirements} can now be formally expressed on the previous \textsc{Pn} as invariant formul\ae. Requirement \textbf{\texttt{R1}}, concerned with file opening by a sufficiently trusted user, is split into two properties $\mathtt{P1}$ and $\mathtt{P2}$, corresponding to each opening mode (resp. write / read mode). 

\begin{small}\hspace{-0.6cm}
$\begin{array}{r @{~\eqqdef~} l}
	\mathtt{P1}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{writing} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
	\mathtt{P2}  & \forall~ \mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{reading} \cdot \mathtt{ac_{u}} \rhd \mathtt{ac_{f}}\\
\end{array}$\end{small}

\smallskip\noindent
Here, requirement \textbf{\texttt{R1}} holds if for any pair $\mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u}) \in \mathtt{File}\times \mathtt{User}$ in the $\mathtt{writing}$ or $\mathtt{reading}$ place, $\mathtt{\$u}$'s access class dominates $\mathtt{\$f}$'s access class.

Requirement \textbf{\texttt{R2}} is implemented by a third property $\mathtt{P3}$ that ensures the confinement property on the \textsc{Pn}.

\smallskip
\hspace{-0.6cm}
\begin{small}
	$\mathtt{P3} ~\eqqdef \begin{array}{l}
		\forall~ \mathtt{\$p}=(\mathtt{\$f}, \mathtt{\$u})\in \mathtt{reading}, \forall~ \mathtt{\$p'}=(\mathtt{\$f'}, \mathtt{\$u'})\in \mathtt{writing} ~\cdot\\ \mathtt{\$un} = \mathtt{\$un'} \Longrightarrow \mathtt{\$ac_{f}} \rhd \mathtt{\$ac_f'}
	\end{array}$\end{small}


\smallskip\noindent
This property says that for all pairs of files simultaneously opened by the same user, when one is on read mode and the other on write mode, the read file's access class dominates the write file's one.

Running \Alpina on the naive \textsc{Fs} shows, as summarised in \Tab \ref{tab:satisfaction}, that none of these properties are satisfied: this \textsc{Fs} only implements as simple \textsc{Fs} mechanism without access control.
%As summarised in \Tab \ref{tab:satisfaction} (Row 1), when running \Alpina on the naive \textsc{Fs}, none of these properties are satisfied: this \textsc{Fs} only implements as simple \textsc{Fs} mechanism without access control.

\begin{table}[t]%
\begin{center}
	\begin{tabular}{l c c c}
		 & \texttt{P1} & \texttt{P2} & \texttt{P3}\\
		\hline\hline
		\texttt{FS} & \tickNo & \tickNo & \tickNo\\
		\texttt{FS$_{\mathtt{s}}$} & \tickYes & \tickYes & \tickNo\\
		\texttt{FS$_{\mathtt{c}}$} & \tickYes & \tickYes & \tickYes\\
		\hline
	\end{tabular}
\end{center}
	\vspace{-.3cm}
	\caption{Property Satisfaction for the three \textsl{File System} versions.}
	\label{tab:satisfaction}
	
	\vspace{-.5cm}
\end{table}
